COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%Axioms for equality%
C00003 ENDMK
C⊗;
%Axioms for equality%

declare INDVAR x y z;

axiom
equal:	∀x. x = x,

	∀x y. (x = y ⊃ y = x),

	∀ x y z. (x = y ∧ y = z ⊃ x = z);;